Inference at * 
Iof proof for Lemma nil member-variant:


  T, A:Type, x:T. (A r T)  ((x  [])  False) 

latex

 by Unfold `l_member` 0 THEN Auto THEN All Reduce  THEN ExRepD THEN Auto 

latex

 .

Definitions	(x  l), P  Q, P & Q, P  Q, , Type, s = t, l[i], [], type List, a < b, ||as||, #$n, x:A. B(x), A c B, x:A  B(x), Void, x:A. B(x), x:AB(x), , {x:A| B(x)} , , A  B, A, False, P  Q, t  T
Lemmas	nat wf, length wf2, select wf, false wf